\documentclass{article}
\usepackage{url}
\usepackage{manfnt}
\usepackage{fullpage}
\usepackage{proof}
\usepackage{amssymb}
\usepackage{latexsym}
\usepackage{xcolor}
\usepackage{mathrsfs}
\usepackage{amsmath, amsthm}
\usepackage{diagrams}

\newcommand{\frank}[1]{\textcolor{blue}{\textbf{[#1 --Frank]}}}
% My own macros
\newcommand{\m}[2]{ \{\mu_{#1}\}_{#1 \in #2}} 
\newcommand{\M}[3]{\{#1_i \mapsto #2_i\}_{i \in #3}} 

\newtheorem{prop}{Proposition}
\newtheorem{definition}{Definition}
\newtheorem{corollary}{Corollary}
\newtheorem{lemma}{Lemma}
\newtheorem{theorem}{Theorem}

\newarrowfiller{dasheq} {==}{==}{==}{==}
\newarrow {Mapsto} |--->
\newarrow {Line} -----
\newarrow {Implies} ===={=>}
\newarrow {EImplies} {}{dasheq}{}{dasheq}{=>}
\newarrow {Onto} ----{>>}
\newarrow {Dashto}{}{dash}{}{dash}{>}
\newarrow {Dashtoo}{}{dash}{}{dash}{>>}
 
\begin{document}
%\pagestyle{empty}
\title{Confluence for Local Lambda-Mu Calculus}
\author{Peng Fu \\
Computer Science, The University of Iowa}
\date{last edited: \today}


\maketitle
\thispagestyle{empty}
\begin{abstract}
  This note is taken directly from my comprehensive exam, modulo some re-organizations.
\end{abstract}
 
\section{Hardin's Interpretation Method}
Sometimes it is inevitable to deal with reduction systems that contains more than one reduction, for example, $(\Lambda, \{ \to_{\beta}, \to_{\eta}\})$. Confluence problem for this kind of system require some nontrivial efforts to prove. Hardin's interpretion method \cite{Hardin:1989} provide a way to deal with some of those reduction systems. 

\begin{lemma}[Interpretation lemma]
\label{interp}
Let $\to $ be $ \to_1 \cup \to_2$, 
$\to_1$ being confluent and strongly normalizing. We denote by $\nu(a)$ the $\to_1$-normal form of $a$. Suppose that there is some relation $\to_i$ on $\to_1$ normal forms satisfying:

\

$\to_i \subseteq \twoheadrightarrow$, and $a \to_2 b $ implies $ \nu(a)   {\twoheadrightarrow_i}    \nu(b)$ $(\dagger)$

\

\noindent Then the confluence of $\to_i$ implies the confluence of $\to$.
\end{lemma}

\begin{proof}
 So suppose $\to_i$ is confluent. If $a  {\twoheadrightarrow}  a'$ and $a  {\twoheadrightarrow}  a''$. So by ($\dagger$), $\nu(a)  {\twoheadrightarrow_i}  \nu(a')$ and $\nu(a)  {\twoheadrightarrow_i}  \nu(a'')$. Notice that $t  {\to_1^*}  t'$ implies $\nu(t) = \nu(t')$(By confluence and strong normalizing of $\to_1$). By confluence of $\to_i$, there exists $b$ such that $\nu(a')  {\twoheadrightarrow_i}  b$ and $\nu(a'')  {\twoheadrightarrow_i}  b$. Since $\to_i, \to_1 \subseteq \twoheadrightarrow$, we got $a' {\twoheadrightarrow}   \nu(a')  {\twoheadrightarrow}  b$ and $a'' {\twoheadrightarrow}   \nu(a'')  {\twoheadrightarrow}  b$. Hence $\to$ is confluent.

\begin{diagram}[size=2em,textflow]
& & & & a & & & &\\
& & &\ldLine &  & \rdLine & & &\\
& &\ldLine & &  & & \rdLine & &\\
&\ldOnto & & & \dDashtoo^1 &  &  & \rdOnto & \\
a'& &  & & \nu(a)  &  & & & a'' \\
&\rdDashtoo^1 &  &\ldDashtoo^i &   & \rdDashtoo^i  &  & \ldDashtoo^1 &\\
& & \nu(a')  &  &   &  & \nu(a'') & & \\
& &  & \rdDashtoo^i  &  & \ldDashtoo^i &   &  & \\
& &  &  & b  &   &  & & \\
\end{diagram}

\end{proof}

Hardin's method reduce the confluence problem of $\to_1 \cup \to_2$ to $\to_i$, given the confluence and strong
normalizing of $\to_1$, this make it possible to apply Tait-Martin-L\"of's (Takahashi's) method to prove confluence of $\to_i$. 


\section{Local $\lambda \mu$ Calculus}
%(6-7 pages)
\label{Local}
We now show an applicaiton of Hardin's method on a concrete example, this example arise naturally in proving 
type preservation for $\mathsf{Selfstar}$. The approach we adopt is similar to the one in \cite{CurienHL96}. 
\begin{definition}[Local Lambda Mu Terms]

\

\noindent \textit{Terms} $t \ :: = \ x \ |  \ \lambda x.t \ | \ t t'  \ | \ \mu t$

\noindent \textit{Closure} $\mu \ ::= \M{x}{t}{\mathcal{I}}$

\end{definition}

The closure is basically a set of recursively defined definitions. Let $\mathcal{I}$ be a finite nonempty index set. For $\M{x}{t}{\mathcal{I}}$, we require for any $ 1 \leq i \leq n $, the set of free variables of $t_i$, $\mathsf{FV}(t_i) \subseteq dom(\mu) = \{x_1,..., x_n\}$ and we do not allow reduction, definition substitution, substitution inside the closure, we call it \textit{local property}, without this property, we are in the dangerous of losing confluence property(see \cite{Ariola:1997} for a detailed discussion). $\mu \in t$ means the closure $\mu$ appears in $t$. $\vec{\mu}t$ denotes $\mu_1...\mu_n t$. $[t'/x](\mu t )\ \equiv \mu([t'/x]t)$. So $\mathsf{FV}(\mu t) = \mathsf{FV}(t) - dom(\mu)$.

\begin{definition}[Beta-Reductions]

\

\begin{tabular}{llllll}
\infer{(\lambda x.t)t' \to_{\beta} [t'/x]t}{}

&

 \infer{\mu x_i \to_{\beta} \mu t_i}{(x_i \mapsto t_i) \in \mu}

&

\infer{\lambda x.t \to_{\beta} \lambda x.t'}{t \to_{\beta}t' }

&

\infer{t t' \to_{\beta} t'' t'}{t \to_{\beta}t''}

&

 \infer{t t' \to_{\beta} t t''}{t'\to_{\beta}t''}

&

\infer{\mu t \to_{\beta} \mu t'}{t \to_{\beta}t' }
\\

\end{tabular}

\end{definition}

\begin{definition}[Mu-Reductions]

\

\begin{tabular}{llll}

 \infer{\mu t \to_{\mu} t}{dom(\mu) \# \mathsf{FV}(t)}

&

 \infer{ \mu(\lambda x.t) \to_{\mu} \lambda x.\mu t}{}

&

\infer{ \mu(t_1 t_2)  \to_{\mu} (\mu t_1 ) (\mu t_2)}{}

&

 \infer{\lambda x.t \to_{\mu} \lambda x.t'}{t \to_{\mu} t'}

\\
\\
\infer{t t' \to_{\mu} t t''}{t'\to_{\mu} t''}

&
\infer{t t' \to_{\mu} t'' t'}{t \to_{\mu} t''}

&

\infer{\mu t \to_{\mu} \mu t'}{t \to_{\mu}t' }

&
\\

\end{tabular}

\end{definition}


\subsubsection{Confluence of Local $\lambda_{\mu}$ Calculus}


\begin{lemma}
  $\to_{\mu}$ is strongly normalizing and confluent.
\end{lemma}

\begin{definition}[$\mu$-Normal Forms]
  
\

\noindent $n \ :: = \ x \ | \   \mu x_i \ | \ \lambda x.n \ | \ n n'$

\end{definition}

\noindent We require $x_i \in dom(\mu)$. 

\begin{definition}[$\mu$-Normalize Funciton]

\

\begin{tabular}{ll}

 $ m(x) \ : = \  x$

& $m(\lambda y.t)\ : = \ \lambda y.m(t)$

\\

 $m(t_1 t_2)\ : = \ m(t_1) m(t_2)$

& 
 $ m(\vec{\mu}y) \ := y$ if $y \notin dom(\vec{\mu})$.

\\
 $ m(\vec{\mu}y) \ := \mu_i y$ if $y \in dom(\mu_i)$.

&  
 $m(\vec{\mu}(t t')) \ :=  m(\vec{\mu} t) m( \vec{\mu}t')$
\\
 $m(\vec{\mu}( \lambda x.t)) \ := \lambda x.  m(\vec{\mu}t)$.

\\
\end{tabular}

\end{definition}

\begin{lemma}
\label{norm:fun}
 Let $\Phi$ denote the set of $\mu$ normal form, for any term $t$, $m(t)\in \Phi$.
\end{lemma}

\begin{proof}
  One way to prove this is first identify $t$ as $\dot{\overrightarrow{\mu_1}}t'$, here $\dot{\overrightarrow{\mu_1}}$ means
there are zero or more closures and $t'$ does not contains any closure at head position.
 Then we can proceed by induction on the structure of $t'$:

\

\noindent \textbf{Base Cases}: $t' = x$, obvious.

\

\noindent \textbf{Step Cases}: If $t' = \lambda x.t''$, 
then $m(\dot{\overrightarrow{\mu_1}}(\lambda x.t'')) \equiv \lambda x.m(\dot{\overrightarrow{\mu_1}} t'')$. Now we can
again identify $t''$ as $\dot{\overrightarrow{\mu_2}} t'''$, where $t'''$ does not have any closure at head position. Since $t'''$ is structurally smaller than $\lambda x.t''$, by IH, $m(\dot{\overrightarrow{\mu_1}}\dot{\overrightarrow{\mu_2}} t''') \in \Phi$, thus $m(\dot{\overrightarrow{\mu_1}}(\lambda x.t'')) \equiv \lambda x.m(\dot{\overrightarrow{\mu_1}} t'') \in \Phi$.

For $t' = t_1 t_2$, we can argue similarly as above.

\end{proof}

\begin{definition}[$\beta$ Reduction on $\mu$-normal Forms]

\
  
\begin{tabular}{llll}

\infer{n \to_{\beta \mu} m(t)}{n \to_{\beta}t}
&
\infer{\lambda x.n \to_{\beta \mu} \lambda x.n'}{n \to_{\beta \mu} n' }

&

\infer{n n' \to_{\beta \mu} n n''}{n' \to_{\beta \mu} n'' }

&

\infer{n n' \to_{\beta \mu} n'' n'}{n \to_{\beta \mu} n'' }

\end{tabular}

\end{definition}

\noindent Note that the last three rules follows from the first rule.  For the second one, because $ n \to_{\beta} t$ implies $ \lambda x.n \to_{\beta} \lambda x.t$ and $m(\lambda x.t) \equiv \lambda x.m(t)$. The others follow similarly. 


\begin{definition}[Parallelization]

\

\begin{tabular}{lll}

\infer{ n \Rightarrow_{\beta \mu} n}{}

&

 \infer{\mu x_i \Rightarrow_{\beta\mu} m(\mu t_i)}{(x_i \mapsto t_i) \in \mu}

&

\infer{(\lambda x.n_1) n_2 \Rightarrow_{\beta\mu} m([n_1'/x]n_2')}{  n_1\Rightarrow_{\beta\mu} n_1' & n_2\Rightarrow_{\beta\mu} n_2'}

\\
\\


\infer{\lambda x.n \Rightarrow_{\beta\mu} \lambda x.n'}{n \Rightarrow_{\beta\mu}n' }

&

\infer{n n' \Rightarrow_{\beta\mu} n'' n'''}{n' \Rightarrow_{\beta\mu} n''' & n \Rightarrow_{\beta\mu}n'' }
\end{tabular}
\end{definition}

\begin{lemma}
  $\to_{\beta\mu} \subseteq \Rightarrow_{\beta\mu} \subseteq \to_{\beta\mu}^*$.
\end{lemma}

\begin{lemma}
\label{norm:sub}
If $n_2 \Rightarrow_{\beta\mu} n_2'$, then $m([n_2/x]n_1) \Rightarrow_{\beta\mu} m([n_2'/x]n_1)$.
\end{lemma}
\begin{proof}
\noindent  By induction on the structure of $n_1$. We list a few non-trivial cases:

\

\noindent \textbf{Base Cases}: $n_1= x$, $n_1 = \mu x_i$, Obvious. 

\

\noindent \textbf{Step Case}: $n_1= \lambda y.n$. We have $ m(\lambda y.[n_2/x]n) \equiv \lambda y.m([n_2/x]n) \stackrel{IH}{\Rightarrow_{\beta\mu}} \lambda y.m([n_2'/x]n) \equiv m(\lambda y.[n_2'/x]n)$.

\

\noindent \textbf{Step Case}: $n_1= n n'$. We have $ m([n_2/x]n [n_2/x]n') \equiv m([n_2/x]n) m([n_2/x]n')\stackrel{IH}{\Rightarrow_{\beta\mu}} m([n_2'/x]n) m([n_2'/x]n')\equiv m([n_2'/x]n[n_2'/x]n)$.

\end{proof}

\begin{lemma}
\label{norm:iden}
 $m(m(t)) \equiv m(t)$ and $m([m(t_1)/y] m(t_2)) \equiv m([t_1/y]t_2)$. 
\end{lemma}
\begin{proof}
The first equality is by lemma \ref{norm:fun}. For the second equality, we 
prove it through similar method as lemma \ref{norm:fun}: We identify $t_2$ as $\dot{\overrightarrow{\mu_1}}t_2'$, 
 $t_2'$ does not contains any closure at head position. We proceed by induction on the structure of $t_2'$:

\

\noindent \textbf{Base Cases}: For $t_2' = x$, we use $m(m(t)) \equiv m(t)$. 

\

\noindent \textbf{Step Cases}: If $t_2' = \lambda x.t_2''$, 
then $m(\dot{\overrightarrow{\mu_1}}(\lambda x.[t_1/y]t_2'')) \equiv \lambda x.m(\dot{\overrightarrow{\mu_1}}([t_1/y]t_2'')) \equiv \lambda x.m(\dot{\overrightarrow{\mu_1}}\dot{\overrightarrow{\mu_2}}([t_1/y]t_2'''))$, where $t_2''$ as $\dot{\overrightarrow{\mu_2}} t_2'''$ and $t_2'''$ does not have any closure at head position. Since $t_2'''$ is structurally smaller than $\lambda x.t_2''$, by IH, $m(\dot{\overrightarrow{\mu_1}}\dot{\overrightarrow{\mu_2}}([t_1/y]t_2''')) \equiv m([t_1/y](\dot{\overrightarrow{\mu_1}}\dot{\overrightarrow{\mu_2}}t_2''')) \equiv m([m(t_1)/y] m(\dot{\overrightarrow{\mu_1}}\dot{\overrightarrow{\mu_2}}t_2'''))$. Thus $\lambda x.m(\dot{\overrightarrow{\mu_1}}\dot{\overrightarrow{\mu_2}}([t_1/y]t_2''')) \equiv \lambda x. m([m(t_1)/y] m(\dot{\overrightarrow{\mu_1}}\dot{\overrightarrow{\mu_2}}t_2'''))$. So $m([t_1/y]\dot{\overrightarrow{\mu_1}}(\lambda x.t_2'')) \equiv m( [m(t_1)/y] m(\lambda x.\dot{\overrightarrow{\mu_1}}\dot{\overrightarrow{\mu_2}}t_2''')) \equiv m( [m(t_1)/y] m(\lambda x.\dot{\overrightarrow{\mu_1}}t_2'')) \equiv m( [m(t_1)/y] m(\dot{\overrightarrow{\mu_1}}(\lambda x.t_2'')))$

For $t_2' = t_a t_b$,  we can argue similarly as above.



\end{proof}

\begin{lemma}
\label{key}
If $n_1 \Rightarrow_{\beta\mu} n_1'$ and $ n_2 \Rightarrow_{\beta\mu} n_2'$, then $m([n_2/x]n_1) \Rightarrow_{\beta\mu} m([n_2'/x]n_1')$.
\end{lemma}
\begin{proof}

\noindent We prove this by induction on the derivation of $  n_1 \Rightarrow_{\beta\mu} n_1'$.
  
\

\noindent \textbf{Base Case:}

\

\noindent \infer{  n \Rightarrow_{\beta \mu} n}{}

\

\noindent By the lemma \ref{norm:sub}.

\

\noindent \textbf{Base Case:}

\

\noindent \infer{  \mu x_i\Rightarrow_{\beta\mu} m(\mu t_i)}{x_i \mapsto t_i \in \mu}

\

\noindent Because $y \notin \mathsf{FV}(\mu x_i)$ and $\mu$ is local. 

\


\noindent \textbf{Step Case:}

\

\noindent \infer{  (\lambda x.n_a) n_b \Rightarrow_{\beta\mu} m([n_a'/x]n_b')}{  n_a\Rightarrow_{\beta\mu} n_a' &   n_b\Rightarrow_{\beta\mu} n_b'}

\

\noindent We have $  m((\lambda x.[n_2/y]n_a) [n_2/y] n_b) \equiv (\lambda x.m([n_2/y]n_a)) m([n_2/y] n_b)$

$ \stackrel{IH}{\Rightarrow_{\beta\mu}} m([m([n_2'/y] n_b')/x]m([n_2'/y] n_a')) \equiv m([n_2'/y]([n_b'/x]n_a'))$. The last equality is by lemma \ref{norm:iden}.

\

\noindent \textbf{Step Case:}

\

\noindent \infer{  \lambda x.n \Rightarrow_{\beta\mu} \lambda x.n'}{  n \Rightarrow_{\beta\mu}n' }

\

\noindent We have $  m(\lambda x.[n_2/y]n) \equiv \lambda x.m([n_2/y]n) \stackrel{IH}{\Rightarrow_{\beta\mu}} \lambda x.m([n_2'/y]n') \equiv m(\lambda x.[n_2'/y]n') $

\

\noindent \textbf{Step Case:}

\

\noindent \infer{  n_a n_b \Rightarrow_{\beta\mu} n_a'n_b'}{   n_a\Rightarrow_{\beta\mu} n_a' &   n_b\Rightarrow_{\beta\mu} n_b'}

\

\noindent We have $  m([n_2/y]n_a [n_2/y] n_b) \equiv m([n_2/y]n_a) m([n_2/y] n_b)$

$ \stackrel{IH}{\Rightarrow_{\beta\mu}} m([n_2'/y] n_a') m([n_2'/y] n_b')\equiv m([n_2'/y](n_a'n_b'))$.

\end{proof}

\begin{lemma}
\label{diamond}
  If $ n \Rightarrow_{\beta\mu} n'$ and $ n \Rightarrow_{\beta\mu} n''$, then there exist $n'''$ such that $ n'' \Rightarrow_{\beta\mu} n'''$ and $ n' \Rightarrow_{\beta\mu} n'''$. So $\to_{\beta\mu}$ is confluent.
\end{lemma}
\begin{proof}
  \noindent By induction on the derivation of $  n \Rightarrow_{\beta\mu} n'$. 

\noindent \textbf{Base Case:}

\

\noindent \infer{  n \Rightarrow_{\beta \mu} n}{}

\

\noindent Obvious.

\

\noindent \textbf{Base Case:}

\

\noindent \infer{  \mu x_i\Rightarrow_{\beta\mu} m(\mu t_i)}{}

\

\noindent Obvious. 

\

\noindent \textbf{Step Case:}

\

\noindent \infer{  (\lambda x.n_1) n_2 \Rightarrow_{\beta\mu} m([n_1'/x]n_2')}{   n_1\Rightarrow_{\beta\mu} n_1' &  n_2\Rightarrow_{\beta\mu} n_2'}

\

\noindent Suppose $  (\lambda x.n_1) n_2 \Rightarrow_{\beta\mu}(\lambda x.n_1'') n_2''$, where $  n_1 \Rightarrow_{\beta\mu}n_1''$ and $  n_2 \Rightarrow_{\beta\mu} n_2''$. By lemma \ref{key} and IH, we have $  m([n_1'/x]n_2') \Rightarrow_{\beta\mu} m([n_1'''/x]n_2''')$. We also have $  (\lambda x.n_1'') n_2''\Rightarrow_{\beta\mu} m([n_1'''/x]n_2''')$, where $  n_1'' \Rightarrow_{\beta\mu}n_1'''$ and $  n_1' \Rightarrow_{\beta\mu}n_1'''$ and $  n_2' \Rightarrow_{\beta\mu} n_2'''$ and $  n_2' \Rightarrow_{\beta\mu}n_2'''$ .

\

\noindent Suppose $  (\lambda x.n_1) n_2 \Rightarrow_{\beta\mu}m([n_2''/x]n_1'') $, where $  n_1 \Rightarrow_{\beta\mu}n_1''$ and $  n_2 \Rightarrow_{\beta\mu} n_2''$. By lemma \ref{key} and IH, we have $  m([n_1'/x]n_2') \Rightarrow_{\beta\mu} m([n_1'''/x]n_2''')$ and $  m([n_1''/x]n_2'') \Rightarrow_{\beta\mu} m([n_1'''/x]n_2''')$.

\

\noindent The other cases are either similar to the one above or easy.

\end{proof}


One can also use Takahashi's method(\cite{Takahashi95}) to prove the lemma above. We will not explore that here.

\begin{lemma}
\label{vec}
$m(\vec{\mu}\vec{\mu}t) \equiv m(\vec{\mu}t)$ and $m(\vec{\mu} ([t_2/x]t_1)) \equiv m( [\vec{\mu} t_2/x]\vec{\mu} t_1)$
\end{lemma}

\begin{proof}
We can prove this using the same method as lemma \ref{norm:fun}. We will not prove it here.
\end{proof}

\dbend
\begin{lemma}
\label{Interp}
If $a \to_{\beta} b$, then $ m(a)\to_{\beta\mu} m(b)$.
\end{lemma}
\begin{proof}
\noindent   We prove this by induction on the derivation(depth) of $  a \to_{\beta} b$. We list a few non-trial cases:

\

\noindent \textbf{Base Case:}

\

\noindent \infer{  \mu x_i \to_{\beta} \mu t_i}{(x_i \mapsto t_i) \in \mu}

\

\noindent We have $  m(\mu x_i) \equiv \mu x_i \to_{\beta\mu} m(\mu  t_i)$.

\

\noindent \textbf{Base Case:}

\

\noindent \infer{  (\lambda x.t)t' \to_{\beta} [t'/x]t}{}

\

\noindent We have $  m((\lambda x.t)t') \equiv (\lambda x.m(t))m(t') \to_{\beta\mu} m([m(t)/x]m(t')) \equiv m([t'/x]t)$.

\

\noindent \textbf{Step Case:}

\

\noindent \infer{  \lambda x.t \to_{\beta} \lambda x.t'}{  t \to_{\beta}t' }

\

\noindent By IH, we have $  m(\lambda x.t)  \equiv  \lambda x.m(t)  \stackrel{IH}{\to_{\beta\mu}} \lambda x.m(t') \equiv m(\lambda x.t') $. 

\

\noindent \textbf{Step Case:}

\

\noindent \infer{  \mu t \to_{\beta} \mu t'}{t \to_{\beta}t' }

\

\noindent We want to show $  m(\mu t) \to_{\beta\mu}  m(\mu t') $. If $dom(\mu)\# FV(t)$, then $  m(\mu t) \equiv m(t) \stackrel{IH}{\to_{\beta\mu}}  m(t') \equiv m(\mu t') $. Of course, here we assume beta-reduction does not introduce any new variable.

\

\noindent If $dom(\mu)\cap FV(t) \not = \emptyset$, then identify $t$ as $\dot{\overrightarrow{\mu_1}}t''$, where
$t''$ does not contain any closure at head position. We do case analyze on the structure of $t''$: 

%\noindent $t \not = \m{y}{t'}{\bar{\mu}.y_i}$ since it will violate our assumption. 
\

\textbf{Case.} $t''=x_i \in dom(\dot{\overrightarrow{\mu_1}})$ or $x_i \notin dom(\dot{\overrightarrow{\mu_1}})$, these cases will not arise.

\

\textbf{Case.} $t'' = \lambda y.t_1$, then it must be that $ t' = \dot{\overrightarrow{\mu_1}}(\lambda y.t_1')$ where $ t_1 \to_{\beta} t_1'$. So 
we get $   \mu \dot{\overrightarrow{\mu_1}} t_1 \to_{\beta} \mu \dot{\overrightarrow{\mu_1}}t_1'$. By IH(depth of $ \mu \dot{\overrightarrow{\mu_1}} t_1 \to_{\beta} \mu \dot{\overrightarrow{\mu_1}}t_1'$ is smaller), we have $  m(\mu \dot{\overrightarrow{\mu_1}}t_1) \to_{\beta\mu} m(\mu \dot{\overrightarrow{\mu_1}}t_1')$. Thus $  m(\mu\dot{\overrightarrow{\mu_1}}(\lambda y.t_1)) \equiv \lambda y.m(\mu\dot{\overrightarrow{\mu_1}} t_1) \to_{\beta\mu} \lambda y.m(\mu\dot{\overrightarrow{\mu_1}} t_1') \equiv m(\mu\dot{\overrightarrow{\mu_1}} (\lambda y.t_1'))$. 

\

\textbf{Case.} $t'' = t_1 t_2$ and $t' = \dot{\overrightarrow{\mu_1}}(t_1' t_2)$, where $ t_1 \to_{\beta} t_1'$. We have  $  \mu\dot{\overrightarrow{\mu_1}} t_1 \to_{\beta } \mu\dot{\overrightarrow{\mu_1}} t_1'$. By IH(depth of $\mu\dot{\overrightarrow{\mu_1}} t_1 \to_{\beta } \mu\dot{\overrightarrow{\mu_1}} t_1'$ is smaller),
$  m(\mu\dot{\overrightarrow{\mu_1}} t_1) \to_{\beta \mu} m(\mu\dot{\overrightarrow{\mu_1}} t_1')$. Thus $  m(\mu\dot{\overrightarrow{\mu_1}}(t_1 t_2)) \equiv m(\mu\dot{\overrightarrow{\mu_1}} t_1) m(\mu\dot{\overrightarrow{\mu_1}} t_2) \to_{\beta \mu} m(\mu\dot{\overrightarrow{\mu_1}} t_1') m(\mu \dot{\overrightarrow{\mu_1}}t_2) \equiv m(\mu\dot{\overrightarrow{\mu_1}}(t_1' t_2))$.
For $t'' = t_1 t_2'$, where $  t_2 \to_{\beta} t_2'$, we can argue similarly. 

\

\textbf{Case.} $t'' = (\lambda y.t_1)t_2$ and $t' = \dot{\overrightarrow{\mu_1}}([t_2/y]t_1)$. $  m(\mu\dot{\overrightarrow{\mu_1}} ((\lambda y.t_1)t_2)) \equiv (\lambda y.m(\mu\dot{\overrightarrow{\mu_1}} t_1)))m(\mu \dot{\overrightarrow{\mu_1}}t_2)  \to_{\beta\mu} m( [m(\mu \dot{\overrightarrow{\mu_1}}t_2)/y] m(\mu \dot{\overrightarrow{\mu_1}} t_1)) \equiv m([\mu\dot{\overrightarrow{\mu_1}} t_2/y] \mu \dot{\overrightarrow{\mu_1}}t_1) \equiv m(\mu \dot{\overrightarrow{\mu_1}} [t_2/y]t_1)$(lemma \ref{vec}).

\end{proof}

\begin{theorem}
  $\to_{\beta} \cup \to_{\mu}$ is confluent. 
\end{theorem}
\begin{proof}
  We know by diamond property of $\Rightarrow_{\beta\mu}$, $\to_{\beta\mu}$ is confluent. Since
$\to_{\mu}$ is strongly normalizing and confluent, and by lemma \ref{Interp} and Hardin's 
interpretation lemma(lemma \ref{interp}), we conclude $\to_{\beta} \cup \to_{\mu}$ is confluent. 

\end{proof}


\bibliographystyle{plain}
\bibliography{lambda-mu}


\end{document}
